Nuprl Lemma : eq_cons_imp_eq_hds
2,24
postcript
pdf
A
:Type,
a
,
b
:
A
,
as
,
bs
:
A
List. (
a
.
as
) = (
b
.
bs
)
a
=
b
latex
Definitions
hd(
l
)
,
False
,
A
,
A
B
,
||
as
||
,
i
j
,
t
T
,
Prop
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
length
cons
,
non
neg
length
,
ge
wf
,
length
wf1
,
hd
wf
origin
A:Type, a, b:A, as, bs:A List. (a.as) = (b.bs) 
a = b A:Type, a, b:A, as, bs:A List. (a.as) = (b.bs) a = b 
A
B
j
T Qx:A. B(x)